#include "ksat.h"
#include "infer.h"
#include <stdio.h>
#include <stdlib.h>

/* restriciton of the turnover */
void setup_turnover_numbers (int N, int L, int R[N + 1], int C[N][L - 1][R[N] + 1], int S[L][N], struct ksat *ksat)
{
	int i, j, base;

	int T[L - 2]; /* turnover variable */

	/* restriction of the maximum R[i] turnovers for one nodees */
	for (i = 0; i < N; i++)
	{
		base = ksat->num_variables;

		for (j = 0; j < L - 2; j++)
		{
			T[j] = base + j;
		}

		ksat->num_variables += L - 2;

		for (j = 0; j < L - 2; j++)
		{
			setup_turnover (S[j][i], S[j + 1][i], T[j], ksat);
		}

		counter_positive1 (L - 2, T, R[i], R[N], C[i], ksat);
	}
}

/* restriction of the number of links */
void setup_links_number (int N, int r[N][N], int g[N][N], int links, struct ksat *ksat)
{
	if (links < 0)
		links = -links;

	int i, j, base, list[3];
	int edge[N * N], X[N * N + 1][links + 1];

	base = ksat->num_variables;

	for (i = 0; i < N; i++)
	{
		for (j = 0; j < N; j++)
		{
			edge[i * N + j] = base + i * N + j;

			list[0] = -edge[i * N + j]; list[1] =  r[i][j]; list[2] =  g[i][j];
			add_clause (ksat, 3, list);

			list[0] =  edge[i * N + j]; list[1] = -r[i][j];
			add_clause (ksat, 2, list);

			list[0] =  edge[i * N + j]; list[1] = -g[i][j];
			add_clause (ksat, 2, list);
		}
	}

	ksat->num_variables += N * N;

	counter_positive2 (N * N, edge, links, links, X, ksat);
}

/* restriction for order */
void setup_turnover_orders (int N, int L, int MAX_R, int C[N][L - 1][MAX_R + 1], int M, int R2[M][5], struct ksat *ksat)
{
	int i, j;

	int X[L - 2], Y[L - 2];

	for (i = 0; i < M; i++)
	{
		for (j = 1; j < L - 1; j++)
		{
			X[j - 1] = C[R2[i][0]][j][R2[i][1]];
			Y[j - 1] = C[R2[i][2]][j][R2[i][3]];
		}
		if (R2[i][4] == 0)
			check_order2 (L - 2, X, Y, ksat);
		else if (R2[i][4] == 1)
			check_order1 (L - 2, X, Y, ksat);
	}
}

/* prevention the early fix point */
void prevent_early_fixpoint (int N, int L, int S[L][N], struct ksat *ksat)
{
	int i, X[N], base, list[N];

	base = ksat->num_variables;

	for (i = 0; i < N; i++)
	{
		X[i] = base + i;
		list[i] = X[i];
	}
	add_clause (ksat, N, list);

	for (i = 0; i < N; i++)
	{
		list[0] = -X[i]; list[1] =  S[L - 3][i]; list[2] =  S[L - 2][i];
		add_clause (ksat, 3, list);

		list[0] = -X[i]; list[1] = -S[L - 3][i]; list[2] = -S[L - 2][i];
		add_clause (ksat, 3, list);
	}

	ksat->num_variables += N;
}

/* set fix point */
void set_fixpoint (int N, int L, int S[L][N], struct ksat *ksat)
{
	int i, list[2];

	for (i = 0; i < N; i++)
	{
		list[0] =  S[L - 1][i]; list[1] = -S[L - 2][i];
		add_clause (ksat, 2, list);

		list[0] = -S[L - 1][i]; list[1] =  S[L - 2][i];
		add_clause (ksat, 2, list);
	}
}

/* setup the known values in the pathway */
void set_pathway (int N, int L, int pathway[L][N], int S[L][N], struct ksat *ksat)
{
	int i, j, list[1];

	for (i = 0; i < L; i++)
	{
		for (j = 0; j < N; j++)
		{
			if (pathway[i][j] == 1)
			{
				list[0] =  S[i][j];
				add_clause (ksat, 1, list);
			}
			else if (pathway[i][j] == 0)
			{
				list[0] = -S[i][j];
				add_clause (ksat, 1, list);
			}
		}
	}
}

/* no all '0'/'1' node in the patheay */
void forbidden_noflip (int N, int L, int S[L][N], struct ksat *ksat)
{
	int i, j, list[L - 1];

	for (i = 0; i < N; i++)
	{
		for (j = 0; j < L - 1; j++)
		{
			list[j] =  S[j][i];
		}
		add_clause (ksat, L - 1, list);

		for (j = 0; j < L - 1; j++)
		{
			list[j] = -S[j][i];
		}
		add_clause (ksat, L - 1, list);
	}
}

/* setup the restrictions required by the trigger node */
void setup_trigger (int N, int L, int S[L][N], int g[N][N], int r[N][N], struct ksat *ksat)
{
	int i, j, list[3];

	list[0] = r[0][0];
	add_clause (ksat, 1, list);

	for (i = 1; i < N; i++)
	{
		/* g[i][0] = S[1][i]bar_S[0][i] */
		list[0] =  g[i][0]; list[1] =  S[0][i]; list[2] = -S[1][i];
		add_clause (ksat, 3, list);

		list[0] = -g[i][0]; list[1] = -S[0][i];
		add_clause (ksat, 2, list);

		list[0] = -g[i][0]; list[1] =  S[1][i];
		add_clause (ksat, 2, list);

		/* r[i][0] = S[0][i]bar_S[1][i] */
		list[0] =  r[i][0]; list[1] = -S[0][i]; list[2] =  S[1][i];
		add_clause (ksat, 3, list);

		list[0] = -r[i][0]; list[1] =  S[0][i];
		add_clause (ksat, 2, list);

		list[0] = -r[i][0]; list[1] = -S[1][i];
		add_clause (ksat, 2, list);
	}

	for (i = 1; i < N; i++)
	{
		for (j = i + 1; j < N; j++)
		{
			/* if g[i][0] and g[j][0] are both ture, then r[i][j] and r[j][i] should be false */
			list[0] = -g[i][0]; list[1] = -g[j][0]; list[2] = -r[i][j];
			add_clause (ksat, 3, list);

			list[0] = -g[i][0]; list[1] = -g[j][0]; list[2] = -r[j][i];
			add_clause (ksat, 3, list);
		}
	}
}

/* initialize array pathway[L][N] based on the struct infer */
void init_pathway (int N, int L, int pathway[L][N], struct infer *infer)
{
	int i, j;

	for (i = 0; i < L; i++)
	{
		for (j = 0; j < N; j++)
		{
			pathway[i][j] = -1;
		}
	}

	for (i = 0; i < N; i++)
	{
		pathway[0][i] = infer->init[i];
	}

	for (i = 0; i < N; i++)
	{
		if (infer->flips[i] % 2 == 0)
			pathway[L - 1][i] = pathway[0][i];
		else
			pathway[L - 1][i] = 1 - pathway[0][i];

		pathway[L - 2][i] = pathway[L - 1][i];
	}

	if (infer->trigger == 1)
	{
		for (i = 1; i < L - 2; i++)
		{
			pathway[i][0] = 0;
		}
	}
}

/* setup all k-SAT equations */
struct ksat* setup_ksat (int N, int L, int pathway[L][N], int S[L][N], int g[N][N], int r[N][N], struct infer *infer)
{
	int i, j, M;
	int R1[N + 1];

	for (i = 0; i < L; i++)
	{
		for (j = 0; j < N; j++)
		{
			S[i][j] = i * N + j + 1;
		}
	}

	for (i = 0; i < N; i++)
	{
		for (j = 0; j < N; j++)
		{
			g[i][j] = L * N + i * N + j + 1;
			r[i][j] = L * N + N * N + i * N + j + 1;
		}
	}

	int dynamics[L - 1][3 * N];

	for (i = 0; i < L - 1; i++)
	{
		for (j = 0; j < N; j++)
		{
			dynamics[i][j] = S[i][j];
			dynamics[i][j + N] = S[i + 1][j];
			if (i == L - 1)
				dynamics[i][j + 2 * N] = S[i + 1][j];
			else
				dynamics[i][j + 2 * N] = S[i + 2][j];
		}
	}
	if (infer->trigger) dynamics[0][N] = 1;

	for (i = 0; i < N + 1; i++)
	{
		R1[i] = infer->flips[i];
	}

	M = infer->M;
	
	int R2[M][5];

	for (i = 0; i < M; i++)
	{
		R2[i][0] = infer->timeorder[i].n1;
		R2[i][1] = infer->timeorder[i].flip1;
		R2[i][2] = infer->timeorder[i].n2;
		R2[i][3] = infer->timeorder[i].flip2;
		R2[i][4] = infer->timeorder[i].type;
	}

	struct ksat *ksat;

	ksat = init_ksat ();
	ksat->num_variables += 2 * N * N + L * N;

	/* restriction of the strong inhibition rules */
	sim_model (infer->trigger, N, L - 1, dynamics, g, r, ksat);

	if (infer->model == 1 || infer->model == 3)
	{
		reliable_trans (infer->trigger, N, L - 2, dynamics, g, r, ksat);

		/* restriction of the quickflips */
		forbidden_quickflips (infer->trigger, N, L, S, ksat);
	}

	if (infer->model >= 2)
	{
		convergence (infer->trigger, N, L - 2, dynamics, g, r, ksat);
	}

	int C[N][L - 1][R1[N] + 1];

	/* restriction of the number of flips */
	setup_turnover_numbers (N, L, R1, C, S, ksat);
	
	/* restriction of the timeorder of flips */
	setup_turnover_orders (N, L, R1[N], C, M, R2, ksat);

	/* setup the known values in the pathway */
	set_pathway (N, L, pathway, S, ksat);

	/* setup fix point */
	set_fixpoint (N, L, S, ksat);

	/* prevent early fixpoint */
	if (infer->fixL == 1) prevent_early_fixpoint (N, L, S, ksat);

	/* restriction of the number of links */
	if (infer->links != 0) setup_links_number (N, r, g, infer->links, ksat);

	/* setup restrictions about the trigger node */
	if (infer->trigger == 1) setup_trigger (N, L, S, g, r, ksat);

	return ksat;
}
